// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_LEX_NAT_H
#define _sHT_LEX_NAT_H

#include <limits.h>
#include <stddef.h>
#include <stdint.h>

#ifdef __FRAMAC__
#  include <sHT/lex/digit.h>
#  include <sHT/math/expnat.h>
#  include <sHT/math/expnat/power10.h>
#  include <sHT/math/expnat/power16.h>
#  include <sHT/math/positional.h>
#  include <sHT/math/vector.h>
#  include <sHT/math/vector-memory.h>
#endif

/*@ axiomatic DigitStar {
      predicate decimal_num_p(\list<ℤ> c) =
        ∀ ℤ i; 0 <= i < \length(c) ==> decimal_p(\nth(c, i));
      predicate downhex_num_p(\list<ℤ> c) =
        ∀ ℤ i; 0 <= i < \length(c) ==> downhex_p(\nth(c, i));
      predicate uphex_num_p(\list<ℤ> c) =
        ∀ ℤ i; 0 <= i < \length(c) ==> uphex_p(\nth(c, i));
      predicate hex_num_p(\list<ℤ> c) =
        ∀ ℤ i; 0 <= i < \length(c) ==> hex_p(\nth(c, i));

      lemma uphex_hex_num:
        ∀ \list<ℤ> c; uphex_num_p(c) ==> hex_num_p(c);
      lemma downhex_hex_num:
        ∀ \list<ℤ> c; downhex_num_p(c) ==> hex_num_p(c);
      lemma decimal_uphex_num:
        ∀ \list<ℤ> c; decimal_num_p(c) ==> uphex_num_p(c);
      lemma decimal_downhex_num:
        ∀ \list<ℤ> c; decimal_num_p(c) ==> downhex_num_p(c);
      lemma decimal_hex_num:
        ∀ \list<ℤ> c; decimal_num_p(c) ==> hex_num_p(c);
    } */

/*@ axiomatic DigitSequence {
      // TODO: non-axiomatic delete once lambda's are supported
      // (= map decimal_val c)
      logic \list<ℤ> decimal_val_plural(\list<ℤ> c);
      axiom decimal_val_plural_length: ∀ \list<ℤ> c;
        \length(decimal_val_plural(c)) == \length(c);
      axiom decimal_val_plural_at: ∀ \list<ℤ> c, ℤ i;
        0 <= i < \length(c) ==> \nth(decimal_val_plural(c), i) == decimal_val(\nth(c, i));
      lemma decimal_val_plural_split: ∀ \list<ℤ> c, d;
        decimal_val_plural(c ^ d)
        == (decimal_val_plural(c) ^ decimal_val_plural(d));
      lemma decimal_val_plural_peelr: ∀ \list<ℤ> c, ℤ d;
        decimal_val_plural(c ^ [| d |])
        == (decimal_val_plural(c) ^ [| decimal_val(d) |]);

      logic \list<ℤ> uphex_val_plural(\list<ℤ> c);
      axiom uphex_val_plural_length: ∀ \list<ℤ> c;
        \length(uphex_val_plural(c)) == \length(c);
      axiom uphex_val_plural_at: ∀ \list<ℤ> c, ℤ i;
        0 <= i < \length(c) ==> \nth(uphex_val_plural(c), i) == uphex_val(\nth(c, i));
      lemma uphex_val_plural_split: ∀ \list<ℤ> c, d;
        uphex_val_plural(c ^ d)
        == (uphex_val_plural(c) ^ uphex_val_plural(d));
      lemma uphex_val_plural_peelr: ∀ \list<ℤ> c, ℤ d;
        uphex_val_plural(c ^ [| d |])
        == (uphex_val_plural(c) ^ [| uphex_val(d) |]);

      logic \list<ℤ> downhex_val_plural(\list<ℤ> c);
      axiom downhex_val_plural_length: ∀ \list<ℤ> c;
        \length(downhex_val_plural(c)) == \length(c);
      axiom downhex_val_plural_at: ∀ \list<ℤ> c, ℤ i;
        0 <= i < \length(c) ==> \nth(downhex_val_plural(c), i) == downhex_val(\nth(c, i));
      lemma downhex_val_plural_split: ∀ \list<ℤ> c, d;
        downhex_val_plural(c ^ d)
        == (downhex_val_plural(c) ^ downhex_val_plural(d));
      lemma downhex_val_plural_peelr: ∀ \list<ℤ> c, ℤ d;
        downhex_val_plural(c ^ [| d |])
        == (downhex_val_plural(c) ^ [| downhex_val(d) |]);

      logic \list<ℤ> hex_val_plural(\list<ℤ> c);
      axiom hex_val_plural_length: ∀ \list<ℤ> c;
        \length(hex_val_plural(c)) == \length(c);
      axiom hex_val_plural_at: ∀ \list<ℤ> c, ℤ i;
        0 <= i < \length(c) ==> \nth(hex_val_plural(c), i) == hex_val(\nth(c, i));
      lemma hex_val_plural_split: ∀ \list<ℤ> c, d;
        hex_val_plural(c ^ d)
        == (hex_val_plural(c) ^ hex_val_plural(d));
      lemma hex_val_plural_peelr: ∀ \list<ℤ> c, ℤ d;
        hex_val_plural(c ^ [| d |])
        == (hex_val_plural(c) ^ [| hex_val(d) |]);
    } */

/*@ // Desc: upper bounds for vectorised digit lexing
    // Status: automatic
    axiomatic DigitSequenceLt {
      lemma decimal_val_plural_lt_at0: ∀ \list<ℤ> c, ℤ j;
        decimal_num_p(c) ==> 0 <= j < \length(decimal_val_plural(c))
        ==> \nth(decimal_val_plural(c), j) < 10;
      lemma decimal_val_plural_lt_at1: ∀ \list<ℤ> c, ℤ j;
        decimal_num_p(c) ==> 0 <= j < \length(c)
        ==> \nth(decimal_val_plural(c), j) < 10;
      lemma decimal_val_plural_lt: ∀ \list<ℤ> c;
        decimal_num_p(c) ==> vector_lt_constant(decimal_val_plural(c), 10);

      lemma uphex_val_plural_lt_at0: ∀ \list<ℤ> c, ℤ j;
        uphex_num_p(c) ==> 0 <= j < \length(uphex_val_plural(c))
        ==> \nth(uphex_val_plural(c), j) < 16;
      lemma uphex_val_plural_lt_at1: ∀ \list<ℤ> c, ℤ j;
        uphex_num_p(c) ==> 0 <= j < \length(c)
        ==> \nth(uphex_val_plural(c), j) < 16;
      lemma uphex_val_plural_lt: ∀ \list<ℤ> c;
        uphex_num_p(c) ==> vector_lt_constant(uphex_val_plural(c), 16);

      lemma downhex_val_plural_lt_at0: ∀ \list<ℤ> c, ℤ j;
        downhex_num_p(c) ==> 0 <= j < \length(downhex_val_plural(c))
        ==> \nth(downhex_val_plural(c), j) < 16;
      lemma downhex_val_plural_lt_at1: ∀ \list<ℤ> c, ℤ j;
        downhex_num_p(c) ==> 0 <= j < \length(c)
        ==> \nth(downhex_val_plural(c), j) < 16;
      lemma downhex_val_plural_lt: ∀ \list<ℤ> c;
        downhex_num_p(c) ==> vector_lt_constant(downhex_val_plural(c), 16);

      lemma hex_val_plural_lt_at0: ∀ \list<ℤ> c, ℤ j;
        hex_num_p(c) ==> 0 <= j < \length(hex_val_plural(c))
        ==> \nth(hex_val_plural(c), j) < 16;
      lemma hex_val_plural_lt_at1: ∀ \list<ℤ> c, ℤ j;
        hex_num_p(c) ==> 0 <= j < \length(c)
        ==> \nth(hex_val_plural(c), j) < 16;
      lemma hex_val_plural_lt: ∀ \list<ℤ> c;
        hex_num_p(c) ==> vector_lt_constant(hex_val_plural(c), 16);
    } */

/*@ // Desc: positivity of lexed digits in a sequence
    // Proof issues: Alt-Ergo drowns by trying to split vectors,
    //  setting a limit of 0 helps, as does interfacing with
    //  Why3.
    // Proof status: auto
    axiomatic DigitSequencePositive {
      lemma decimal_plural_positive: ∀ \list<ℤ> c;
        decimal_num_p(c) ⇒ vector_ge0(decimal_val_plural(c));
      lemma uphex_val_plural_positive: ∀ \list<ℤ> c;
        uphex_num_p(c) ⇒ vector_ge0(uphex_val_plural(c));
      lemma downhex_val_plural_positive: ∀ \list<ℤ> c;
        downhex_num_p(c) ⇒ vector_ge0(downhex_val_plural(c));
      lemma hex_val_plural_positive: ∀ \list<ℤ> c;
        hex_num_p(c) ⇒ vector_ge0(hex_val_plural(c));
    } */

/*@ // Description: Order: most-significant to least-significant
    // Proof status: auto
    axiomatic Numeric {
      logic ℤ decimal_num_val(\list<ℤ> c)
        = sum_digits_ms_to_ls(10, decimal_val_plural(c));
      logic ℤ uphex_num_val(\list<ℤ> c)
        = sum_digits_ms_to_ls(16, uphex_val_plural(c));
      logic ℤ downhex_num_val(\list<ℤ> c)
        = sum_digits_ms_to_ls(16, downhex_val_plural(c));
      logic ℤ hex_num_val(\list<ℤ> c)
        = sum_digits_ms_to_ls(16, hex_val_plural(c));

      // These are specialisations of `sum_digits_ms_to_ls_ind`.
      lemma decimal_val_peelr: ∀ \list<ℤ> c, ℤ d;
        decimal_num_val(c ^ [| d |]) == 10 * decimal_num_val(c) + decimal_val(d);
      lemma uphex_num_val_peelr: ∀ \list<ℤ> c, ℤ d;
        uphex_num_val(c ^ [| d |]) == 16 * uphex_num_val(c) + uphex_val(d);
      lemma downhex_num_val_peelr: ∀ \list<ℤ> c, ℤ d;
        downhex_num_val(c ^ [| d |]) == 16 * downhex_num_val(c) + downhex_val(d);
      lemma hex_num_val_peelr: ∀ \list<ℤ> c, ℤ d;
        hex_num_val(c ^ [| d |]) == 16 * hex_num_val(c) + hex_val(d);
    } */

/*@ // Desc: upper bounds on lexed numbers
    //   > These are specialisations of sum_digits_lt
    // Proof status: auto
    axiomatic NumericLt {
      lemma decimal_num_val_lt: ∀ \list<ℤ> c;
        decimal_num_p(c) ==> decimal_num_val(c) < expnat(10, \length(c));
      lemma uphex_num_val_lt: ∀ \list<ℤ> c;
        uphex_num_p(c) ==> uphex_num_val(c) < expnat(16, \length(c));
      lemma downhex_num_val_lt: ∀ \list<ℤ> c;
        downhex_num_p(c) ==> downhex_num_val(c) < expnat(16, \length(c));
      lemma hex_num_val_lt: ∀ \list<ℤ> c;
        hex_num_p(c) ==> hex_num_val(c) < expnat(16, \length(c));
    } */

/*@ // Desc: positivity of lexed numbers
    //   > These are specialisations of sum_digits_positive
    // Proof status: auto
    axiomatic NumericPositive {
      lemma decimal_num_val_positive: ∀ \list<ℤ> c;
        decimal_num_p(c) ⇒ 0 ≤ decimal_num_val(c);
      lemma uphex_num_val_positive: ∀ \list<ℤ> c;
        uphex_num_p(c) ⇒ 0 ≤ uphex_num_val(c);
      lemma downhex_num_val_positive: ∀ \list<ℤ> c;
        downhex_num_p(c) ⇒ 0 ≤ downhex_num_val(c);
      lemma hex_num_val_positive: ∀ \list<ℤ> c;
        hex_num_p(c) ⇒ 0 ≤ hex_num_val(c);
    } */

/*@ lemma uphex_to_u32_nooverflow_help: ∀ ℤ n;
      0 ≤ n ≤ 8 ⇒ expnat(16, n) ≤ UINT32_MAX + 1; */
/*@ lemma uphex_to_u32_nooverflow: ∀ \list<ℤ> d;
      uphex_num_p(d) ∧ 0 ≤ \length(d) ≤ 8 ⇒ uphex_num_val(d) ≤ UINT32_MAX; */

/** Parse a big-endian, upper-case, hexadecimal number < 2**32

  Hint: if $0 ≤ e - b ≤ 8$, `bounds` holds by
  `uphex_to_u32_nooverflow`. */
/*@ requires order: b <= e;
    requires bounds: NS ⇒ uphex_num_val(vector_load_u8(c + b, e - b)) <= UINT32_MAX;
    requires from_r: \valid_read(&c[b .. e - 1]);
    requires from_rS: S ==> \valid_read(&c[0 .. e - 1]);
    requires from_r0S: S ==> \valid_read(&c[0]);
    requires num: NS ==> uphex_num_p(vector_load_u8(c + b, e - b));
    terminates NS;
    assigns \result \from c[0 .. e - 1], c[0];
    ensures result: NS ==> \result
      == uphex_num_val(vector_load_u8(c + b, e - b)); */
uint32_t
sHT_uphex_to_u32(uint8_t *c, size_t b, size_t e);

/*@ lemma decimal_to_u32_nooverflow_help: ∀ ℤ n;
      0 ≤ n ≤ 9 ⇒ expnat(10, 9) ≤ UINT32_MAX + 1; */
/*@ lemma decimal_to_u32_nooverflow: ∀ \list<ℤ> d;
      decimal_num_p(d) ∧ 0 ≤ \length(d) ≤ 9 ⇒ decimal_num_val(d) ≤ UINT32_MAX; */

/** Parse a big-endian decimal number < 2**32

  Beware, this function does not reject leading zeroes.

  Hint: if $0 ≤ e - b ≤ 9$, `bounds` holds by
  `decimal_to_u32_nooverflow`. */
/*@ requires order: b <= e;
    requires bounds: NS ⇒ decimal_num_val(vector_load_u8(c + b, e - b)) <= UINT32_MAX;
    requires from_r: \valid_read(&c[b .. e - 1]);
    requires from_rS: S ==> \valid_read(&c[0 .. e - 1]);
    requires from_r0S: S ==> \valid_read(&c[0]);
    requires num: NS ==> decimal_num_p(vector_load_u8(c + b, e - b));
    terminates NS;
    assigns \result \from c[0 .. e - 1], c[0];
    ensures result: NS ==> \result
      == decimal_num_val(vector_load_u8(c + b, e - b)); */
uint32_t
sHT_decimal_to_u32(uint8_t *c, size_t b, size_t e);

#endif
